(declare-fun n () Int)
(declare-fun a_1 () Int)
(declare-fun f (Int) Int)
(declare-fun g_1 (Int) Int)
(assert (forall ((i Int)) (xor (and (= (f 0) 238) (= (f 15) 33) (>= 93 (f i)) (< 0 132) (xor (distinct i n (f i) 145) (xor (= (f (+ 240 i 121)) 19))) (distinct (g_1 248) 254) (xor (= 0 38) (= (g_1 (* i 235)) 190)) (or (= (f i) 114) (= (g_1 (div i 129)) (+ 33 217))) (xor (distinct (f i) 143) (distinct (g_1 (div i 216)) (g_1 i))) (or (= (f i) 62) (> (g_1 i) a_1)) (xor (distinct (f i) 124) (or (>= (g_1 i) a_1) (< (g_1 i) 232)))))))
(check-sat)
(declare-fun n () Int)
(declare-fun a_1 () Int)
(declare-fun f (Int) Int)
(declare-fun g_1 (Int) Int)
(assert (forall ((i Int)) (xor (and (= (f 0) 238) (= (f 15) 33) (>= 93 (f i)) (< 0 132) (xor (distinct i n (f i) 145) (xor (= (f (+ 240 i 121)) 19))) (distinct (g_1 248) 254) (xor (= 0 38) (= (g_1 (* i 235)) 190)) (or (= (f i) 114) (= (g_1 (div i 129)) (+ 33 217))) (xor (distinct (f i) 143) (distinct (g_1 (div i 216)) (g_1 i))) (or (= (f i) 62) (> (g_1 i) a_1)) (xor (distinct (f i) 124) (or (>= (g_1 i) a_1) (< (g_1 i) 232)))))))
(check-sat)
